\begin{tabbing}
$\forall$\=$C$:(Id$\rightarrow$Type), $A$, $B$:Type, $L_{2}$:(${\it tg}$:Id$\times$($A$$\rightarrow$$B$$\rightarrow$($C$(${\it tg}$) List))) List, $L$:(IdLnk$\times$$t$:Id$\times$$C$($t$)) List,\+
\\[0ex]${\it tg}$:Id, $a$:$A$, $b$:$B$.
\-\\[0ex]\{\=map($\lambda$$x$.2of($x$);$L$)\+
\\[0ex]$=$
\\[0ex]concat(map($\lambda$${\it tgf}$.map($\lambda$$x$.$\langle$1of(${\it tgf}$)$,\,$$x$$\rangle$;2of(${\it tgf}$)($a$,$b$));$L_{2}$))
\\[0ex]$\in$ (${\it tg}$:Id$\times$$C$(${\it tg}$)) List
\\[0ex]$\Rightarrow$ $\neg$(${\it tg}$ $\in$ map($\lambda$$p$.1of($p$);$L_{2}$))
\\[0ex]$\Rightarrow$ $\parallel$filter($\lambda$${\it ms}$.1of(2of(${\it ms}$)) = ${\it tg}$;$L$)$\parallel$ $=$ 0\}
\-
\end{tabbing}